Section: New Results

Generating equality tests for inductive types

Participant : Enrico Tassi.

We show how to derive in a modular fashion equality tests for a wide variety of inductive type definitions. This makes an instrumental use of parametricity. This work has been published in an international conference [10]. This is also an interesting case study for the Elpi language [2].